Deadlock-freeness

Given P() as an orchestration, the following assertion asks whether P() is deadlock-free or not.

#assert P() deadlockfree;

where both assert and deadlockfree are reserved keywords.  PAT's model checker performs a Depth-First-Search algorithm to repeatedly explore unvisited states until a deadlock state (i.e., a state with no further move) is found or all states have been visited.

Reachability

Given P() as an orchestration, the following assertion asks whether P() can reach a state at which some given condition is satisfied.

#assert P() reaches cond;

where both assert and reaches are reserved key words and cond is a proposition defined as a global definition.  For instance, the following asks whether P() can reach a state at which x is negative.

• var x = 0;
• #define goal x < 0;
• P() = add{x = x + 1;} -> P() [] minus{x = x -1;} -> P();
• #assert P() reaches goal;

In order to tell whether the assertion is true or not, PAT's model checker performs a depth-first-search algorithm to repeatedly explore unvisited states until a state at which the condition is true is found or all states have been visited.

LTL

In PAT, we support the full set of LTL syntax. Given an orchestration P(), the following assertion asks whether P() satisfies the LTL formula.

#assert P() |= F;

where F is an LTL formula whose syntax is defined as the following rules,

F = e | prop | [] F | <> F | X F | F1 U F2

where e is an event, prop is a pre-defined proposition, [] reads as "always", <> reads as "eventually", X reads as "next" and U reads as "until".  Informally, the assertion is true if and only if every execution of the system satisfies the formula. Given an LTL formula, PAT's model checker firstly invokes a procedure to generate a Buchi automaton which is equivalent to the negation of the formula. Then, the Buchi automaton is composed of the internal model of P() so as to determine whether the formula is true for all system executions or not. Refer to [SUNLDP09] for details. For instance, the following asks whether the philosopher can always eventually eat or not (i.e., non-starvation).

#assert Phil() |= []<>eat;

Note: event e can be component event like eat.0. e can also be channel event like "c!3" or "c?19". Double quotation marks are needed when writing channal events due to the special characters ! and ?.

#assert Phil() |= []<> eat.0 && "c!3";

Note: e when two or more X are used together, leave a space between them. XX will be mis-recognized as a propersition.

Conformance

In PAT, we support FDR's approach for checking whether an implementation satisfies a specification or not. That is, by the notion of refinement or equivalence. Different from LTL assertions, an assertion for refinement compares behaviors of a given process as a whole with another process, e.g., whether there is a subset relationship.

#assert Orc() refines Chor()  //we test whether orchestration Orc conforms to choroegraphy Chor.

PAT's model checker invokes a reachability analysis procedure to repeatedly explore the (synchronization) product of P() and Q() to search for a state at which the refinement relationship does not hold.